path 依存型
path-dependent type
https://gyazo.com/25460e65c0fefe986a98417c6ab78150
type selection$ x.L
subtyping of types
$ \frac{\Gamma\vdash x\ni{\bf type}~L<:U,U<:U'}{\Gamma\vdash x.L<:U'}({\rm TSEL}_u{\text -}<:).
$ \frac{\Gamma\vdash x\ni{\bf type}~L:S..U,S'<:S,S<:U}{\Gamma\vdash S'<:x.L}(<:{\text -}{\rm TSEL}).
$ \frac{\Gamma\vdash x\ni{\bf type}~L:S..U,U<:U',S<:U}{\Gamma\vdash x.L<:U'}({\rm TSEL}{\text -}<:).
well-formed types
$ \frac{\Gamma\vdash x\ni{\bf type}~L:S..U,S<:U}{\Gamma\vdash x.L~{\bf wf}}({\rm TSEL}{\text -}{\rm WF}).
$ \frac{\Gamma\vdash x\ni{\bf type}~L<:U,U~{\bf wf}}{\Gamma\vdash x.L~{\bf wf}}({\rm TSEL}_u{\rm WF}).
explanation
$ \frac{\Gamma\vdash x\ni{\bf type}~L:S..U,U\prec_x\overline D}{\Gamma\vdash x.L\prec_x\overline D}({\rm TSEL}{\text -}\prec).
$ \frac{\Gamma\vdash x\ni{\bf type}~L<:U,U\prec_x\overline D}{\Gamma\vdash x.L\prec_x\overline D}({\rm TSEL}_u{\text -}\prec).
code:scala
val o: { o =>
type A <: { a => }
def m(x: { a => }): o.A
} = new ( o =>
type A: { a => } .. { a => }
def m(x: { a => }): o.A = x
);
o.m(new ( a => )): o.A
Reconciling Nominality and Refinements
nominality (名前的)
As in µDOT, a type selection can be treated nominally, based on its name, even in the context of subtyping types where the selected type member has different bounds. In particular, this subtyping proposition should hold as it does in µDOT:
$ \{z\Rarr{\rm type}A:X..X;\quad{\rm def}~{\rm id}(z.A):z.A\}<:\{z\Rarr{\rm type}A<:\{a\Rarr\};\quad{\rm def}~{\rm id}(z.A):z.A\}.
where$ Xis a valid but irrelevant type. Notice the resemblance with establishing that Cow is a subtype of Animal.
general refinements
If we admit types$ \{z\Rarr T\land T'\}instead of just$ \{z\Rarr D\}we obtain general open refinements, powerful enough to express types arising through OOP constructs like inheritance and mixins.
general (總稱)、refinement (細別 (篩型)) かな? environment narrowing
$ \frac{\Gamma^a,(x:U),\Gamma^b\vdash T<:T'\quad\Gamma^a\vdash S<:U}{\Gamma^a,(x:S),\Gamma^b\vdash T<:T'}({\rm <:{\text -}NARROW}).
The particular problematic case occurs when refining a path-dependent type$ x.L. Assuming a certain type$ Tfor$ x, a refinement$ Uof$ Tmight look valid, but environment narrowing tells us that we can replace the binding of$ xwith type$ S<:T, which might be a refinement of$ Tthat is incompatible with$ U.
code:scala
trait A {
type B
def f(b: B): Unit = {}
}
trait Ba
trait Aa extends A {
type B = Ba
}
val aa = new Aa {}
aa.f(new Ba {}) // OK
val aaa: A = aa
aaa.f(new Ba {})
// Found: Object with Playground.Ba {...}
// Required: Playground.aaa.B
code:scala
class A {
class B {
def f(b: B): Unit = {}
}
def newB: B = new B()
}
val a1 = new A()
a1.newB.f(a1.newB) // OK
val a2 = a1
a1.newB.f(a2.newB)
// Found: Playground.a2.B
// Required: Playground.a1.B
a2.newB.f(a1.newB)
// Found: Playground.a1.B
// Required: Playground.a2.B
値を parameter として持つ型
code:scala
case class Z(modulus: Int) {
sealed class Modulus {
val value = modulus
}
object Modulus {
implicit val mod: Modulus = new Modulus()
}
}
def +(x: IntModN)(implicit m: N): IntModN = value + x }
object IntMod {
import scala.language.implicitConversions
modulus: N
new IntModN(i % modulus.value) implicit def intModN2Long(a: IntMod_): Long = a.value }
val z1 = Z(2)
val z2 = Z(10)
println(i1z1 + i2z2)
package の外から型を注入する例。package の利用者は實行時型解決の樣に記述できる
code:scala
trait time_t_proto {
type time_t
}
trait time_t_implU extends time_t_proto { type time_t = U
}
case class PtrU(time: U) extends time_t_implU trait Platform extends time_t_proto
object PlatformI386 extends Platform with time_t_implInt object PlatformX64 extends Platform with time_t_implLong val arch = "x86_64"
val platform: Platform =
if arch == "i386" then PlatformI386
else if arch == "x86_64" then PlatformX64
else ???
f(t) // 42: platform.time_t
依存函數型 (dependent function type)$ \Pi x:T_1.T_2
dependent method
code:scala
trait V
trait A {
type B = V
def newB = new B {}
}
def f(a: A): a.B = a.newB
f(new A {}) // : V
code:scala
trait A { type B; val b: B }
val f: (a: A) => a.B = (a: A) => a.b
總稱型 (generics)
code:scala
abstract class Key(name: String) { type Value }
def keyV(name: String) = new Key(name) { override type Value = V } class DB {
def set(k: Key, v: k.Value): Unit = {
println(k)
println(v)
}
}
val db = new DB
db.set(k1, "v1")
db.set(k2, 42.0)
以下と同じ
code:scala
case class KeyV(name: String) {} class DB {
def setV(k: KeyV, v: V): Unit = { println(k)
println(v)
}
}
val db = new DB
db.set(k1, "v1")
db.set(k2, 42.0)
型射影 (type projection) A#B